/*!
 * \file symbol_table.cc
 *
 * \brief Implentation of the SymbolTable and STE classes
 *        that are used in the SparseConstraints class.
 *
 * \date Started: 6/8/2010
 * \date Last Modified: 10/1/2010
 * \authors Alan LaMielle
 * \authors Ian Craig
 * \authors Nicholas Jeanette
 *
 * Copyright (c) 2010, Colorado State University <br>
 * All rights reserved. <br>
 * See ../../COPYING for details. <br>
 */

#include <iegenlib/iegenlib.h>

#include <sstream>
#include <assert.h>
#include <algorithm>
using std::equal;
using std::stringstream;
using std::max;

namespace iegenlib{

/********************************** ExpVec ************************************/
ExpVec::ExpVec(int s1, int s2, int s3, int s4, int conValue):
               const_coeff(conValue){
  symconst_coeffs = vector<int>(s1,0);
  tuplevars_coeffs = vector<int>(s2,0);
  existvars_coeffs = vector<int>(s3,0);
  ufcalls_coeffs = vector<int>(s4,0);
}

ExpVec::ExpVec(ExpVec const& other):
               symconst_coeffs(other.symconst_coeffs),
               tuplevars_coeffs(other.tuplevars_coeffs),
               existvars_coeffs(other.existvars_coeffs),
               ufcalls_coeffs(other.ufcalls_coeffs),
               const_coeff(other.const_coeff){
}

//ExpVec assignment operator that doesn't reduce the size of the target's coeff
// vectors if the source's coeff vectors are shorter
ExpVec& ExpVec::operator=(ExpVec const& other){
  this->symconst_coeffs=other.symconst_coeffs;
  this->tuplevars_coeffs=other.tuplevars_coeffs;
  this->existvars_coeffs=other.existvars_coeffs;
  this->ufcalls_coeffs=other.ufcalls_coeffs;
  this->const_coeff=other.const_coeff;
  return *this;
}

//Similar to ExpVec assignment operator except that this doesn't reduce the size
// of the target's coeff vectors if the source's coeff vectors are shorter
ExpVec ExpVec::copy_coeff(ExpVec const& other) const{
  ExpVec res(*this);

  list<vector<int>*> coeff_vecs_res;
  list<vector<int>const*> coeff_vecs_other;

  //Build a pair of lists of pointers to coefficient vectors
  //Symbolic constants
  coeff_vecs_res.push_back(&(res.symconst_coeffs));
  coeff_vecs_other.push_back(&other.symconst_coeffs);

  //Tuple variables
  coeff_vecs_res.push_back(&(res.tuplevars_coeffs));
  coeff_vecs_other.push_back(&other.tuplevars_coeffs);

  //Existential variables
  coeff_vecs_res.push_back(&(res.existvars_coeffs));
  coeff_vecs_other.push_back(&other.existvars_coeffs);

  //UFCalls
  coeff_vecs_res.push_back(&(res.ufcalls_coeffs));
  coeff_vecs_other.push_back(&(other.ufcalls_coeffs));

  //Do the assignment: first assign 0s
  res.symconst_coeffs=vector<int>(res.symconst_coeffs.size(),0);
  res.tuplevars_coeffs=vector<int>(res.tuplevars_coeffs.size(),0);
  res.existvars_coeffs=vector<int>(res.existvars_coeffs.size(),0);
  res.ufcalls_coeffs=vector<int>(res.ufcalls_coeffs.size(),0);

  //Do the assignment: assign from source ExpVec
  list<vector<int>*>::iterator coeff_vec_res;
  list<vector<int>const*>::iterator coeff_vec_other;
  for(coeff_vec_res=coeff_vecs_res.begin(),
      coeff_vec_other=coeff_vecs_other.begin();
      coeff_vec_res!=coeff_vecs_res.end() &&
      coeff_vec_other!=coeff_vecs_other.end();
      ++coeff_vec_res,++coeff_vec_other)
  {
    for(int i=0;
        i<(*coeff_vec_res)->size() && i<(*coeff_vec_other)->size();
        ++i){
      (*coeff_vec_res)->at(i)=(*coeff_vec_other)->at(i);
    }
  }

  //Do the assignment: constant value
  res.const_coeff=other.const_coeff;

  return res;
}

ExpVec::~ExpVec(){}

void ExpVec::set_coeff(SymType type, int col, int coeff){
  switch(type){
    case SYMBOLIC:
      symconst_coeffs[col] = coeff;
      break;
    case TUPLE:
      tuplevars_coeffs[col] = coeff;
      break;
    case EXISTENTIAL:
      existvars_coeffs[col] = coeff;
      break;
    case UFCALL:
      ufcalls_coeffs[col] = coeff;
      break;
    default:
      throw StringException("Cannot use ExpVec.set_coeff to set the constant, use ExpVec.set_const instead");
      break;
  }
}

int ExpVec::get_coeff(SymType type, int col) const{
  switch(type){
    case SYMBOLIC:
      return symconst_coeffs[col];
    case TUPLE:
      return tuplevars_coeffs[col];
    case EXISTENTIAL:
      return existvars_coeffs[col];
    case UFCALL:
      return ufcalls_coeffs[col];
      break;
    default:
      throw StringException("Cannot use ExpVec.get_coeff to get the constant, use ExpVec.get_const instead");
      break;
  }
}

const bool ExpVec::operator<(const ExpVec& op2) const {
  if(this->const_coeff < op2.const_coeff){ return true; }
  else if(this->const_coeff > op2.const_coeff){ return false;}
  if(this->symconst_coeffs < op2.symconst_coeffs){ return true; }
  else if(this->symconst_coeffs > op2.symconst_coeffs){ return false; }
  if(this->tuplevars_coeffs < op2.tuplevars_coeffs){ return true; }
  else if(this->tuplevars_coeffs > op2.tuplevars_coeffs){ return false; }
  if(this->existvars_coeffs < op2.existvars_coeffs){ return true; }
  else if(this->existvars_coeffs > op2.existvars_coeffs){ return false; }
  if(this->ufcalls_coeffs < op2.ufcalls_coeffs){ return true; }
  else if(this->ufcalls_coeffs > op2.ufcalls_coeffs){ return false; }
  return false;
}

const bool ExpVec::operator==(const ExpVec& op2) const {
  return symconst_coeffs.size() == op2.symconst_coeffs.size() &&
         tuplevars_coeffs.size() == op2.tuplevars_coeffs.size() &&
         existvars_coeffs.size() == op2.existvars_coeffs.size() &&
         ufcalls_coeffs.size() == op2.ufcalls_coeffs.size() &&
         equal(symconst_coeffs.begin(), symconst_coeffs.end(),
               op2.symconst_coeffs.begin()) &&
         equal(tuplevars_coeffs.begin(), tuplevars_coeffs.end(),
               op2.tuplevars_coeffs.begin()) &&
         equal(existvars_coeffs.begin(), existvars_coeffs.end(),
               op2.existvars_coeffs.begin()) &&
         equal(ufcalls_coeffs.begin(), ufcalls_coeffs.end(),
               op2.ufcalls_coeffs.begin()) &&
         const_coeff == op2.const_coeff;
}

ExpVec ExpVec::operator*(int coeff){
  ExpVec temp(this->symconst_coeffs.size(),this->tuplevars_coeffs.size(),
              this->existvars_coeffs.size(),this->ufcalls_coeffs.size());

  for(int i=0; i<this->get_symconst_size(); i++){
    temp.set_coeff(SYMBOLIC,i,coeff*this->get_coeff(SYMBOLIC,i));
  }
  for(int i=0; i<this->get_tuplevars_size(); i++){
    temp.set_coeff(TUPLE,i,coeff*this->get_coeff(TUPLE,i));
  }
  for(int i=0; i<this->get_existvars_size(); i++){
    temp.set_coeff(EXISTENTIAL,i,coeff*this->get_coeff(EXISTENTIAL,i));
  }
  for(int i=0; i<this->get_ufcalls_size(); i++){
    temp.set_coeff(UFCALL,i,coeff*this->get_coeff(UFCALL,i));
  }
  temp.set_const(coeff*this->get_const());

  return temp;
}

vector<int> ExpVec::add_coeff_vecs(vector<int> vec1,vector<int> vec2) const{
  vector<int> res,source;

  if(vec1.size()>vec2.size()){
    res=vec1;
    source=vec2;
  }
  else{
    res=vec2;
    source=vec1;
  }

  for(int i=0; i<source.size(); ++i){
    res[i]+=source[i];
  }

  return res;
}

ExpVec operator+(const ExpVec& op1, const ExpVec& op2){
  ExpVec res=ExpVec(0,0,0,0);

  res.symconst_coeffs=res.add_coeff_vecs(op1.symconst_coeffs,op2.symconst_coeffs);
  res.tuplevars_coeffs=res.add_coeff_vecs(op1.tuplevars_coeffs,op2.tuplevars_coeffs);
  res.existvars_coeffs=res.add_coeff_vecs(op1.existvars_coeffs,op2.existvars_coeffs);
  res.ufcalls_coeffs=res.add_coeff_vecs(op1.ufcalls_coeffs,op2.ufcalls_coeffs);
  res.const_coeff=op1.const_coeff+op2.const_coeff;
  return res;
}

string ExpVec::toString() const{
  stringstream temp;
  temp << symconst_coeffs.size() << ", " << tuplevars_coeffs.size() << ", " <<
          existvars_coeffs.size() << ", " << ufcalls_coeffs.size() << ", " <<
          const_coeff;
  return temp.str();
}

string ExpVec::toString(SymbolTable* st) const {
  vector<string> symbols;
  for(int index = 0; index < symconst_coeffs.size(); ++index){
    stringstream num;
    STE* temp = st->lookup(SYMBOLIC, index);
    if(symconst_coeffs.at(index) != 0 && temp != 0){
      num << symconst_coeffs.at(index);
      if(symconst_coeffs.at(index) > 1){
        symbols.push_back("+" + num.str() + temp->getId());
      }else if(symconst_coeffs.at(index) < 0){
        if(symconst_coeffs.at(index) != -1){
          symbols.push_back(num.str() + temp->getId());
        }else{
          symbols.push_back("-" + temp->getId());
        }
      }else{
        symbols.push_back("+" + temp->getId());
      }
    }
  }
  vector<string> tuples;
  for(int index = 0; index < tuplevars_coeffs.size(); ++index){
    stringstream num;
    STE* temp = st->lookup(TUPLE, index);
    int coeff = 0;
    if(temp != 0 && (coeff=tuplevars_coeffs.at((temp)->getCol())) != 0){
      num << coeff;
      if(coeff > 1){
        symbols.push_back("+" + num.str() + temp->getId());
      }else if(coeff < 0){
        if(coeff != -1){
          symbols.push_back(num.str() + temp->getId());
        }else{
          symbols.push_back("-" + temp->getId());
        }
      }else{
        symbols.push_back("+" + temp->getId());
      }
    }
  }
  vector<string> exists;
  for(int index = 0; index < existvars_coeffs.size(); ++index){
    stringstream num;
    STE* temp = st->lookup(EXISTENTIAL, index);
    if(existvars_coeffs.at(index) != 0 && temp != 0){
      num << existvars_coeffs.at(index);
      if(existvars_coeffs.at(index) > 1){
        symbols.push_back("+" + num.str() + temp->getId());
      }else if(existvars_coeffs.at(index) < 0){
        if(existvars_coeffs.at(index) != -1){
          symbols.push_back(num.str() + temp->getId());
        }else{
          symbols.push_back("-" + temp->getId());
        }
      }else{
        symbols.push_back("+" + temp->getId());
      }
    }
  }
  vector<string> ufcs;
  for(int index = 0; index < ufcalls_coeffs.size(); ++index){
    stringstream num;
    //TODO:get rid of duplicate function name calls
    if(ufcalls_coeffs.at(index) != 0){
      UFCall* temp = static_cast<UFCall*>(st->lookup(UFCALL, index));
      if(temp != 0){
        num << ufcalls_coeffs.at(index);
        if(ufcalls_coeffs.at(index) > 1){
          symbols.push_back("+" + num.str() + temp->getId() +
          ufcallStringHelper(temp->getParams(), st));
        }else if(ufcalls_coeffs.at(index) < 0){
          if(ufcalls_coeffs.at(index) != -1){
            symbols.push_back(num.str() + temp->getId() +
            ufcallStringHelper(temp->getParams(), st));
          }else{
            symbols.push_back("-" + temp->getId() +
            ufcallStringHelper(temp->getParams(), st));
          }
        }else{
          symbols.push_back("+" + temp->getId() +
          ufcallStringHelper(temp->getParams(), st));
        }
      }
    }
  }

  stringstream retval;
  for(vector<string>::iterator it = symbols.begin(); it != symbols.end(); ++it){
    retval << *it;
  }
  if(const_coeff != 0){
    if(const_coeff > 0) retval << "+";
    retval << const_coeff;
  }
  if(retval.str().size() == 0){
    retval << "0";
  }
  if(retval.str().at(0) == '+'){
    return retval.str().substr(1);
  }
  return retval.str();
}

string ExpVec::ufcallStringHelper(list<ExpVec> params, SymbolTable* ST) const {
  string paramString = "(";
  for(list<ExpVec>::iterator it = params.begin(); it != params.end(); ++it){
    paramString += it->toString(ST);
    paramString += ",";
  }
  if(paramString.length() == 1){
    return "";
  }
  return paramString.substr(0, paramString.length()-1) + ")";
}

string ExpVec::vectorStrings(){
  stringstream symbolics, tuples, exists, ufcalls;
  symbolics << "SYMCONSTS  :";
  tuples    << "TUPLEVARS  :";
  exists    << "EXISTENTIAL:";
  ufcalls   << "UFCALLS    :";
  for(vector<int>::const_iterator it = symconst_coeffs.begin();
      it != symconst_coeffs.end(); ++it){
    symbolics << " " << (*it);
  }
  for(vector<int>::const_iterator it = tuplevars_coeffs.begin();
      it != tuplevars_coeffs.end(); ++it){
    tuples << " " << (*it);
  }
  for(vector<int>::const_iterator it = existvars_coeffs.begin();
      it != existvars_coeffs.end(); ++it){
    exists << " " << (*it);
  }
  for(vector<int>::const_iterator it = ufcalls_coeffs.begin();
      it != ufcalls_coeffs.end(); ++it){
    ufcalls << " " << (*it);
  }
  symbolics << "\n";
  tuples    << "\n";
  exists    << "\n";
  ufcalls   << "\n";
  stringstream full;
  full << symbolics.str() << tuples.str() << exists.str() << ufcalls.str() <<
          "CONST      : " << const_coeff;
  return full.str();
}

void ExpVec::normalizeEquality(){
  bool negative = false;
  bool first = false;
  normalizeHelperFindNegative(symconst_coeffs.begin(), symconst_coeffs.end(),
                              &negative , &first);
  if(!negative && !first){
    normalizeHelperFindNegative(tuplevars_coeffs.begin(),
                                tuplevars_coeffs.end(), &negative, &first);
    if(!negative && !first){
      normalizeHelperFindNegative(existvars_coeffs.begin(),
                                  existvars_coeffs.end(), &negative, &first);
      if(!negative && !first){
        normalizeHelperFindNegative(ufcalls_coeffs.begin(),
                                    ufcalls_coeffs.end(), &negative, &first);
      }
    }
  }
  if(negative){
    normalizeHelperInverseArray(&symconst_coeffs);
    normalizeHelperInverseArray(&tuplevars_coeffs);
    normalizeHelperInverseArray(&existvars_coeffs);
    normalizeHelperInverseArray(&ufcalls_coeffs);
    this->const_coeff=this->const_coeff*-1;
  }
}

void ExpVec::normalizeHelperFindNegative(vector<int>::const_iterator begin,
                                         vector<int>::const_iterator end,
                                         bool* negative, bool* first){
  for(;begin != end; ++begin){
    if(*begin != 0){
      if(*begin < 0){
        *negative = true;
        return;
      }
      *first = true;
      return;
    }
  }
}

void ExpVec::normalizeHelperInverseArray(vector<int>* vec){
  for(int i = 0; i < vec->size(); ++i){
    (*vec)[i] = (*vec)[i]*-1;
  }
}

void ExpVec::apply(SRVisitor* visitor) const {
  visitor->ExpVecCase(this);
}

bool ExpVec::any(SymType type,int& pos,int& coeff) const{
  bool res=false;

  vector<int> coeffs;

  if(SYMBOLIC==type || TUPLE==type || EXISTENTIAL==type || UFCALL==type){
    if(SYMBOLIC==type){coeffs=this->get_symconst_coeffs();}
    else if(TUPLE==type){coeffs=this->get_tuplevars_coeffs();}
    else if(EXISTENTIAL==type){coeffs=this->get_existvars_coeffs();}
    else if(UFCALL==type){coeffs=this->get_ufcalls_coeffs();}

    for(int i=0; i<coeffs.size(); ++i){
      if(0!=coeffs[i]){
        res=true;
        pos=i;
        coeff=coeffs[i];
        break;
      }
    }
  }
  else if(CONST==type){
    if(0!=this->get_const()){
      res=true;
      coeff=this->get_const();
    }
  }
  else{
    throw StringException("Unhandled SymType constant value");
  }

  return res;
}

bool ExpVec::any(SymType type,int pos,SymbolTable const*const sym_table) const{
  bool res=false;

  //Check the top-level terms in this expression
  if(SYMBOLIC==type || TUPLE==type || EXISTENTIAL==type || UFCALL==type){
    if(0!=this->get_coeff(type,pos)){
      res=true;
    }
  }
  else if(CONST==type){
    if(0!=this->get_const()){
      res=true;
    }
  }
  else{
    throw StringException("Unhandled SymType constant value");
  }

  //Check the arguments of any UFCalls, if necessary
  if((!res) && (NULL!=sym_table)){
    //Look in each UFS in this expression
    for(int i=0; i<this->get_ufcalls_size(); i++){
      if(0!=this->get_coeff(UFCALL,i)){
        UFCall* ufcall=sym_table->lookup_ufcall(i);
        res=ufcall->any(type,pos,sym_table);
        if(res){break;}
      }
    }
  }

  return res;
}

bool ExpVec::anyNesting(SymType type,int& pos,int& coeff, SymbolTable const*
sym_table) const{

  bool res=false;

  vector<int> coeffs;

  //Check the top-level terms in this expression
  if(SYMBOLIC==type || TUPLE==type || EXISTENTIAL==type || UFCALL==type){
    if(SYMBOLIC==type){coeffs=this->get_symconst_coeffs();}
    else if(TUPLE==type){coeffs=this->get_tuplevars_coeffs();}
    else if(EXISTENTIAL==type){coeffs=this->get_existvars_coeffs();}
    else if(UFCALL==type){coeffs=this->get_ufcalls_coeffs();}

    for(int i=0; i<coeffs.size(); ++i){
      if(0!=coeffs[i]){
        res=true;
        pos=i;
        coeff=coeffs[i];
        break;
      }
    }
  }
  else if(CONST==type){
    if(0!=this->get_const()){
      res=true;
      coeff=this->get_const();
    }
  }

 //Check the arguments of any UFCalls, and
 //call the method anyNesting() recursively for nested UFC functions
  if((!res)){
    //get_ufcalls_size returns size of the UFC coefficient list
    for(int i=0; i< this->get_ufcalls_size(); i++){
       if(0!=this->get_coeff(UFCALL,i)){
         UFCall* ufcall=sym_table->lookup_ufcall(i);
         //recursive call of the method for nested UFC
         res=ufcall->anyNesting(type,pos,coeff, sym_table);
         if(res){break;}
       }
    }
  }
return res;
}


ExpVec ExpVec::replaceExistential(SymbolTable* sym_table,int exist_pos,
                                  ExpVec equal_exp) const{
  ExpVec res(*this);
  int num_initial_ufs_coeffs=res.get_ufcalls_size();

  //Do the lookups/creation of new UFS STEs that have had the given existential
  // replaced in their arguments and update the coefficient of the non-replaced
  // UFS to the replaced UFS

  //For each existing UFS...
  for(int i=0; i<num_initial_ufs_coeffs; ++i){
    //Grab it's coefficient
    int curr_coeff=res.get_coeff(UFCALL,i);

    //If the current UFS expression has a non-zero coefficient..
    if(0!=curr_coeff){
      //Get the UFCall STE for the current UFS
      UFCall* ufs=sym_table->lookup_ufcall(i);

      //Build a list of arguments where the existential has been replaced
      list<ExpVec> replaced_args;

      //For each argument of the current UFS...
      for(list<ExpVec>::const_iterator param=ufs->getParamsBegin();
          param!=ufs->getParamsEnd();
          ++param){
        //Add the replaced ExpVec to the list of replaced arguments
        replaced_args.push_back(param->replaceExistential(sym_table,
                                                          exist_pos,
                                                          equal_exp));
      }

      //Lookup the new UFS where the existential has been replaced
      UFCall* replaced_ufs=sym_table->lookup(ufs->getId(),replaced_args);

      //Construct a new ExpVec with a column reserved for the new UFS
      ExpVec new_res(sym_table->constructExpVec());

      //Copy the current result's coefficients
      new_res=new_res.copy_coeff(res);

      //Clear the coefficient of the old UFS and set the coefficient of the new
      // UFS to the previous coefficient
      new_res.set_coeff(UFCALL,i,0);
      new_res.set_coeff(UFCALL,replaced_ufs->getCol(),curr_coeff);

      //Update the current result
      res=new_res;
    }
  }

  //Do we need to replace in the top level expression?
  int exist_coeff=this->get_coeff(EXISTENTIAL,exist_pos);
  if(0!=exist_coeff){
    ExpVec exist_exp=sym_table->constructExpVec();
    exist_exp.set_coeff(EXISTENTIAL,exist_pos,-1*exist_coeff);

    //Subtract off the existential variable
    res=res+exist_exp;

    //Add in the equivalent expression
    res=res+(equal_exp*exist_coeff);
  }

  return res;
}

bool ExpVec::isAffine() const{
  bool res=true;

  for(int i=0; i<this->get_ufcalls_size(); i++){
    if(0!=this->get_coeff(UFCALL,i)){
      res=false;
      break;
    }
  }

  return res;
}
/******************************************************************************/

/*********************************** STE **************************************/
string STE::toStringCommon(string type_string) const{
  string temp = " ";
  temp.append(type_string);

  stringstream num;
  num << this->col;
  temp += ", " + num.str();
  return this->id + "," + temp;
}
/******************************************************************************/

void TupleVar::apply(SRVisitor* visitor) { visitor->TupleVarCase(this); }
void ExistVar::apply(SRVisitor* visitor) { visitor->ExistVarCase(this); }
void SymConst::apply(SRVisitor* visitor) { visitor->SymConstCase(this); }
void UFCall::apply(SRVisitor* visitor) { visitor->UFCallCase(this); }
void TupleType::apply(SRVisitor* visitor) const { visitor->TupleTypeCase(this);}

string TupleVar::toString() const{return this->toStringCommon("TUPLE");}
string ExistVar::toString() const{return this->toStringCommon("EXISTENTIAL");}
string SymConst::toString() const{return this->toStringCommon("SYMBOLIC");}
string UFCall::toString() const{return this->toStringCommon("UFCALL");}

/********************************* UFCall *************************************/
UFCall::UFCall(string name, int col, list<ExpVec>* params):STE(name,UFCALL,col){
  list<ExpVec> tempParams;
  for(list<ExpVec>::iterator itr = params->begin(); itr != params->end(); ++itr){
    ExpVec ev(*itr);
    //raise exception flag = true
    tempParams.push_back(ev);
  }
  paramIDs = list<ExpVec>();
  paramIDs = tempParams;
}

void UFCall::applyParams(SRVisitor* visitor){
  for(list<ExpVec>::const_iterator it = paramIDs.begin(); it != paramIDs.end();
      ++it){
    visitor->ExpVecCase(&*it);
  }
}

string UFCall::getFullFunc(SymbolTable* st){
  stringstream ufcall;
  ufcall << id << "(";
  for(list<ExpVec>::const_iterator itr = paramIDs.begin();
      itr != paramIDs.end(); ++itr){
    ufcall << itr->toString(st) << ",";
  }
  string retval = ufcall.str();
  return retval.substr(0,retval.length()-1) + ")";
}

bool UFCall::any(SymType type,int pos,SymbolTable const*const sym_table) const{
  bool res=false;

  //Look in each of the UFSs parameters
  for(list<ExpVec>::const_iterator param=this->getParamsBegin();
      param!=this->getParamsEnd(); ++param){
    res=param->any(type,pos,sym_table);
    if(res){break;}
  }
  return res;
}

bool UFCall::anyNesting(SymType type,int& pos,int& coeff, SymbolTable const*
sym_table) const{
  bool res=false;

  //Look in each of the UFSs parameters
  for(list<ExpVec>::const_iterator param=this->getParamsBegin();
      param!=this->getParamsEnd(); ++param){
    res=param->anyNesting(type,pos,coeff, sym_table);
    if(res){break;}
  }
  return res;
}
/******************************************************************************/

/******************************** SymTable ************************************/
SymbolTable::SymbolTable(const set<string>* tuplevars,
                         const set<string>* symconsts,
                         const set<string>* exists,
                         const int funcCount){
  num_tuplevars = tuplevars->size();
  num_symconsts = symconsts->size();
  num_existvars = exists->size();
  num_ufcalls = funcCount;

  doneIncr = true;
  UFCcount = 0;

  int count = 0;
  for(set<string>::const_iterator it = tuplevars->begin();
      it != tuplevars->end(); ++it){
    if(*it != ""){
      STE* temp = new TupleVar(*it, count);
      mSymToSTE[(*it)] = temp;
      pair<SymType, int> p;
      p.first = TUPLE;
      p.second = count;
    mTypeColToSTE[p] = temp;
      count++;
    }
  }
  count = 0;
  for(set<string>::const_iterator it = symconsts->begin();
      it != symconsts->end(); ++it){
    STE* temp = new SymConst((*it), count);
    mSymToSTE[(*it)] = temp;
    pair<SymType, int> p;
    p.first = SYMBOLIC;
    p.second = count;
    mTypeColToSTE[p] = temp;
    count++;
  }
  count = 0;
  for(set<string>::const_iterator it = exists->begin(); it != exists->end();
      ++it){
    STE* temp = new ExistVar((*it), count);
    mSymToSTE[(*it)] = temp;
    pair<SymType, int> p;
    p.first = EXISTENTIAL;
    p.second = count;
    mTypeColToSTE[p] = temp;
    count++;
  }
}

 SymbolTable::SymbolTable(const SymbolTable& ST){

   num_tuplevars = ST.num_tuplevars;
   num_existvars = ST.num_existvars;
   num_symconsts = ST.num_symconsts;
   num_ufcalls = ST.num_ufcalls;
   doneIncr = ST.doneIncr;
   UFCcount = ST.UFCcount;

    //need to destroy current ste to make room for the new ones
    for(map<pair<SymType,int>, STE*>::iterator it = mTypeColToSTE.begin();
       it != mTypeColToSTE.end(); ++it){
       delete it->second;
    }
    mTypeColToSTE.clear();
    mSymToSTE.clear();
    mNameListToSTE.clear();

    for(map<pair<SymType, int>, STE*>::const_iterator it = ST.mTypeColToSTE.begin();
       it != ST.mTypeColToSTE.end(); ++it){

       if(it->first.first==SYMBOLIC){
          STE* tmp = new SymConst((it->second->getId()),(it->second->getCol()));
          mSymToSTE[it->second->getId()] = tmp;
          mTypeColToSTE[it->first] = tmp;
       }else if(it->first.first==EXISTENTIAL){
          STE* tmp = new ExistVar((it->second->getId()),(it->second->getCol()));
          mSymToSTE[it->second->getId()] = tmp;
          mTypeColToSTE[it->first] = tmp;

       }else if(it->first.first==TUPLE){
          STE* tmp = new TupleVar((it->second->getId()),(it->second->getCol()));
          mSymToSTE[it->second->getId()] = tmp;
          mTypeColToSTE[it->first] = tmp;
       }else if(it->first.first==UFCALL){
          UFCall* tuf = (static_cast<UFCall*>(it->second));
          list<ExpVec> tpar = tuf->getParams();
          STE* tmp = new UFCall((it->second->getId()),(it->second->getCol()),
                &tpar);
          //mSymToSTE[it->second->getId()] = tmp;
          mTypeColToSTE[it->first] = tmp;
          pair<string, list<ExpVec> > p;
          p.first = it->second->getId();
          p.second = tpar;
          mNameListToSTE[p] = tmp;
       }
    }
}

SymbolTable::~SymbolTable(){
  //the map type and column to STE map contains ALL STE's unlike the other maps,
  //so deconstructing from this one will ensure that the symbol table is
  //destructed properly
  for(map<pair<SymType,int>, STE*>::iterator it = mTypeColToSTE.begin();
      it != mTypeColToSTE.end(); ++it){
    delete it->second;
  }
}

SymbolTable& SymbolTable::operator=(const SymbolTable& ST){
    if(this != &ST){
       num_tuplevars = ST.num_tuplevars;
       num_existvars = ST.num_existvars;
       num_symconsts = ST.num_symconsts;
       num_ufcalls = ST.num_ufcalls;
       doneIncr = ST.doneIncr;
       UFCcount = ST.UFCcount;

    //need to destroy current ste to make room for the new ones
    for(map<pair<SymType,int>, STE*>::iterator it = mTypeColToSTE.begin();
       it != mTypeColToSTE.end(); ++it){
       delete it->second;
    }
    mTypeColToSTE.clear();
    mSymToSTE.clear();
    mNameListToSTE.clear();

    for(map<pair<SymType, int>, STE*>::const_iterator it = ST.mTypeColToSTE.begin();
       it != ST.mTypeColToSTE.end(); ++it){

       if(it->first.first==SYMBOLIC){
          STE* tmp = new SymConst((it->second->getId()),(it->second->getCol()));
          mSymToSTE[it->second->getId()] = tmp;
          mTypeColToSTE[it->first] = tmp;
       }else if(it->first.first==EXISTENTIAL){
          STE* tmp = new ExistVar((it->second->getId()),(it->second->getCol()));
          mSymToSTE[it->second->getId()] = tmp;
          mTypeColToSTE[it->first] = tmp;
       }else if(it->first.first==TUPLE){
          STE* tmp = new TupleVar((it->second->getId()),(it->second->getCol()));
          mSymToSTE[it->second->getId()] = tmp;
          mTypeColToSTE[it->first] = tmp;
       }else if(it->first.first==UFCALL){
          UFCall* tuf = (static_cast<UFCall*>(it->second));
          list<ExpVec> tpar = tuf->getParams();
          STE* tmp = new UFCall((it->second->getId()),(it->second->getCol()),
                &tpar);
          //mSymToSTE[it->second->getId()] = tmp;
          mTypeColToSTE[it->first] = tmp;
          pair<string, list<ExpVec> > p;
          p.first = it->second->getId();
          p.second = tpar;
          mNameListToSTE[p] = tmp;
       }
    }
    }
    return *this;
}

STE* SymbolTable::lookup(string sym) const{
  map<string,STE*>::const_iterator ste;

  //Find the given symbol name
  ste=mSymToSTE.find(sym);

  //Make sure the symbol being looked up already exists
  if(mSymToSTE.end()==ste){
    throw StringException("Symbol '"+sym+"' does not exist in the symbol table.");
  }

  return ste->second;
}

UFCall* SymbolTable::lookup(string fname, list<ExpVec> params){
  doneIncr = true;
  UFCall* temp;
  if(mNameListToSTE.find(pair<string, list<ExpVec> >(fname, params)) ==
     mNameListToSTE.end()){
    temp = new UFCall(fname, UFCcount, &params);
    mNameListToSTE[make_pair(fname,params)] = temp;
    pair<SymType, int> p;
    p.first = UFCALL;
    p.second = UFCcount;
    mTypeColToSTE[p] = temp;
    if(num_ufcalls <= UFCcount){num_ufcalls++;}
    UFCcount++;
  }else{
    temp = static_cast<UFCall*>(mNameListToSTE[pair<string, list<ExpVec> >(fname, params)]);
  }
  return temp;
}

STE* SymbolTable::lookup(SymType type,int col) const{
  pair<SymType,int> p; p.first = type; p.second = col;
  map<pair<SymType,int>,STE*>::const_iterator ste=mTypeColToSTE.find(p);
  if(ste==mTypeColToSTE.end()){
    return 0; //throw StringException("Cannot find the requested STE*");
  }
  return ste->second;
}

TupleVar* SymbolTable::lookup_tuple(int col) const{
  return static_cast<TupleVar*>(this->lookup(TUPLE,col));
}

SymConst* SymbolTable::lookup_symconst(int col) const{
  return static_cast<SymConst*>(this->lookup(SYMBOLIC,col));
}

ExistVar* SymbolTable::lookup_exist(int col) const{
  return static_cast<ExistVar*>(this->lookup(EXISTENTIAL,col));
}

UFCall* SymbolTable::lookup_ufcall(int col) const{
  return static_cast<UFCall*>(this->lookup(UFCALL,col));
}

ExpVec SymbolTable::constructExpVec() const{
  return ExpVec(num_symconsts, num_tuplevars, num_existvars, num_ufcalls);
}

ExpVec SymbolTable::constructExpVec(string var, int coeff){
  STE* entry = this->lookup(var);
  ExpVec temp(num_symconsts, num_tuplevars, num_existvars, num_ufcalls);
  temp.set_coeff(entry->getType(), entry->getCol(), coeff);
  return temp;
}

ExpVec SymbolTable::constructExpVec(int const_coeff) const{
  return ExpVec(num_symconsts, num_tuplevars, num_existvars, num_ufcalls,
                const_coeff);
}

ExpVec SymbolTable::constructExpVec(string fname, list<ExpVec> params,
                                    int coeff){
  UFCall* entry = this->lookup(fname, params);
  ExpVec temp(num_symconsts, num_tuplevars, num_existvars, num_ufcalls);
  temp.set_coeff(entry->getType(), entry->getCol(), coeff);
  return temp;
}

string SymbolTable::toString() const{
  stringstream temp;
  vector<pair<SymType, int > > keyList;
  for(map<pair<SymType, int >, STE*>::const_iterator it = mTypeColToSTE.begin();
      it != mTypeColToSTE.end(); ++it){
    keyList.push_back(it->first);
  }
  sort(keyList.begin(), keyList.end());
  for(vector<pair<SymType, int> >::const_iterator it = keyList.begin();
      it != keyList.end(); ++it){
    map<pair<SymType,int>,STE*>::const_iterator key_value=mTypeColToSTE.find(*it);
    if(mTypeColToSTE.end()!=key_value){
      temp << key_value->second->toString() << "\n";
    }
    else{
      throw StringException("Invalid key returned by std::map iterator");
    }
  }
  return temp.str();
}

void SymbolTable::apply(SRVisitor* visit){
  visit->SymbolTableCase(this);
}

const map<SymType, int> SymbolTable::getTotals() const{
  map<SymType, int> totals;
  for(map<pair<SymType,int>, STE*>::const_iterator it = mTypeColToSTE.begin();
      it != mTypeColToSTE.end(); ++it){
    totals[it->first.first]++;
  }
  return totals;
}

void SymbolTable::applySTEs(SRVisitor* visit){
  for(map<pair<SymType,int>, STE*>::iterator it = mTypeColToSTE.begin();
      it != mTypeColToSTE.end(); ++it){
    it->second->apply(visit);
  }
}

ExpVec SymbolTable::convertExpVec(ExpVec oldEV, SymbolTable* newST,
                                  map<string,string>* symbolMapping){
  ExpVec retval = newST->constructExpVec();
  /*
   for each tuple, symbolic, and exists column in oldEV:
       lookup the oldSTE for old column in "this"
       use symbolMapping to convert to new varname
       lookup varname in newST
       place coefficient in new column for newSTE in retval
  */
  this->convertExpVecHelper(oldEV, newST, symbolMapping, SYMBOLIC,
                            oldEV.get_symconst_size(), &retval);
  this->convertExpVecHelper(oldEV, newST, symbolMapping, TUPLE,
                            oldEV.get_tuplevars_size(), &retval);
  this->convertExpVecHelper(oldEV, newST, symbolMapping, EXISTENTIAL,
                            oldEV.get_existvars_size(), &retval);
  /*
   for each funcExp column
       assuming we can look up the FuncCall STE with this info, Ian said as much
       for each funcCall STE, call convertExpVec recursively on its ExpVec
       parameters then look up func name and its new parameter ExpVec in the new
       symbol table to get new column put coefficient from oldEV into new column
       in retval
  */
  this->convertExpVecHelper(oldEV, newST, symbolMapping, UFCALL,
                            oldEV.get_ufcalls_size(), &retval);
  retval.set_const(oldEV.get_const());
  return retval;

}

void SymbolTable::convertExpVecHelper(ExpVec oldEV, SymbolTable* newST,
                                      map<string,string>* symbolMapping,
                                      SymType type, int size, ExpVec* retval){
  for(int i = 0; i < size; ++i){
    //If the coefficient is 0, then we don't need to worry about this value and
    //can move onto the next one
    if(oldEV.get_coeff(type,i) == 0) continue;
    STE* thisSTE = this->lookup(type, i);
    string newName;
    string Tuple_from_old_symTable ="not empty";
    STE* otherSTE;
    //If the type of the symbol is not a UFCall...
    if(type != UFCALL){
      //...and is a TupleVar, then find the new name using the mapping from
      //this Symbol Table to the new one
      if(type == TUPLE){
        newName = (*symbolMapping)[thisSTE->getId()];
        Tuple_from_old_symTable = newName;
      //...and is an Existential, then make sure the existential exists in the
      //new symbol table
      }else if(type == EXISTENTIAL){
        //Does the existential still exist in the new symbol table?
        if(newST->containsExistential(thisSTE->getId())){
          //The new symbol table contains the existential
          newName = thisSTE->getId();
        }
        else{
          //The new symbol table does not contain the existential, so skip this
          //column
          continue;
        }
      //...and is a Symbolic, then just get the name of the symbolic
      }else{
        newName = thisSTE->getId();
      }
      //lookup the STE from the new symbol table using the new name
      if(Tuple_from_old_symTable != ""){
         otherSTE = newST->lookup(newName);}
    //If the type of the symbol is a UFCall
    }else{
      UFCall* ufcall = dynamic_cast<UFCall*>(thisSTE);
      list<ExpVec> newParams;
      //For each parameter in the UFCall, convert those expression vectors
      //using this method and add the converted vectors to a new list
      for(list<ExpVec>::const_iterator EVitr = ufcall->getParamsBegin();
          EVitr != ufcall->getParamsEnd(); ++EVitr){
        newParams.push_back(convertExpVec(*EVitr, newST, symbolMapping));
      }
      //lookup the STE from the function name and the converted list of
      //parameters
      otherSTE = newST->lookup(thisSTE->getId(), newParams);
    }
    //Set the coefficient of the proper column to the coefficient in the new
    //symbol table
    if(Tuple_from_old_symTable != ""){
       retval->set_coeff(otherSTE->getType(), otherSTE->getCol(), oldEV.get_coeff(type, i));}
  }
}

list<string>::const_iterator SymbolTable::getIdBegin(){
   makeIdList();
   return mIdList.begin();
}

list<string>::const_iterator SymbolTable::getIdEnd(){
   makeIdList();
   return mIdList.end();
}

list<STE*>::const_iterator SymbolTable::existBegin(){
   makeItList(EXISTENTIAL);
   return mItList.begin();
}

list<STE*>::const_iterator SymbolTable::existEnd() {
   return mItList.end();
}

list<string>::const_iterator SymbolTable::existNamesBegin(){
   makeItNamesList(EXISTENTIAL);
   return mIdList.begin();
}

list<string>::const_iterator SymbolTable::existNamesEnd() {
   return mIdList.end();
}

bool SymbolTable::containsExistential(string name){
  makeItNamesList(EXISTENTIAL);
  set<string> ids(mIdList.begin(),mIdList.end());
  return ids.find(name)!=ids.end();
}

list<STE*>::const_iterator SymbolTable::symBegin(){
   makeItList(SYMBOLIC);
   return mItList.begin();
}

list<STE*>::const_iterator SymbolTable::symEnd(){
   return mItList.end();
}

list<string>::const_iterator SymbolTable::symNamesBegin(){
   makeItNamesList(SYMBOLIC);
   return mIdList.begin();
}

list<string>::const_iterator SymbolTable::symNamesEnd(){
   return mIdList.end();
}

list<UFCall*>::const_iterator SymbolTable::ufcallsBegin(){
  list<UFCall*> ufcallsList;
  for(map<pair<SymType,int>, STE*>::const_iterator it = mTypeColToSTE.begin();
      it != mTypeColToSTE.end(); ++it){
    if((it->first).first == UFCALL){
      ufcallsList.push_back(static_cast<UFCall*>(it->second));
    }
  }
  this->mUFCallsList=ufcallsList;
  return this->mUFCallsList.end();
}

list<UFCall*>::const_iterator SymbolTable::ufcallsEnd(){
  return this->mUFCallsList.end();
}

void SymbolTable::makeIdList(){
   list<string> IdList;
   for(map<pair<SymType,int>, STE*>::const_iterator it = mTypeColToSTE.begin();
      it != mTypeColToSTE.end(); ++it){
         string tmpString = it->second->getId();
         if(it->second->getType() == UFCALL){
            int col=it->second->getCol();
            UFCall *ufs=this->lookup_ufcall(col);
            string idname=ufs->getFullFunc(this);
            IdList.push_back(idname);
         }
         else{
            IdList.push_back(tmpString);
         }
   }
   mIdList = IdList;
}

void SymbolTable::makeItList(SymType exisym){
   list<STE*> ItList;
   for(map<pair<SymType,int>, STE*>::const_iterator it = mTypeColToSTE.begin();
      it != mTypeColToSTE.end(); ++it){
      if((it->first).first == exisym){
         ItList.push_back(it->second);
      }
   }
   mItList = ItList;
}

void SymbolTable::makeItNamesList(SymType exisym){
   list<string> IdList;
   for(map<pair<SymType,int>, STE*>::const_iterator it = mTypeColToSTE.begin();
      it != mTypeColToSTE.end(); ++it){
      if((it->first).first == exisym){
         IdList.push_back(it->second->getId());
      }
   }
   mIdList = IdList;
}
/******************************************************************************/

}//end namespace iegenlib
